1 /-
2 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl
5
6 Hahn decomposition theorem
7
8 TODO:
9 * introduce finite measures (into nnreal)
10 * show general for signed measures (into ℝ)
11 -/
12 import measure_theory.measure_space
src └──────────────────────────┘
13
14 open set lattice filter
15 open_locale classical topological_space
16
17 namespace measure_theory
18
19 variables {α : Type*} [measurable_space α] {μ ν : measure α}
20
21 -- suddenly this is necessary?!
22 private lemma aux {m : ℕ} {γ d : ℝ} (h : γ - (1 / 2) ^ m < d) :
23 γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d :=
24 by linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
25
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
26 lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) :
27 ∃s, is_measurable s ∧
28 (∀t, is_measurable t → t ⊆ s → ν t ≤ μ t) ∧
29 (∀t, is_measurable t → t ⊆ - s → μ t ≤ ν t) :=
30 begin
31 let d : set α → ℝ := λs, ((μ s).to_nnreal : ℝ) - (ν s).to_nnreal,
src └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘
typ └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘
doc └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘
txt └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘
par └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘
pid └───┘└─┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └────────────┘ └┘ ┴ ┴ └────────┘┴
32 let c : set ℝ := d '' {s | is_measurable s },
src └──────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
typ └──────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
doc └──────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
txt └──────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
par └──────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
pid └───┘└─┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
33 let γ : ℝ := Sup c,
src └──────┘ └──┘ ┴
typ └──────┘ └──┘ ┴
doc └──────┘ └──┘ ┴
txt └──────┘ └──┘ ┴
par └──────┘ └──┘ ┴
pid └───┘└─┘ └──┘ ┴
34
35 have hμ : ∀s, μ s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
src └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
doc └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
txt └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
par └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
36 have hν : ∀s, ν s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
id ┴ └────────────┘ └──────────┘ └─────────┘ └┘
src └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘└────────────┘┴ └──────────┘┴ ┴└─────────┘└──┘
typ └────────┘ ┴ ┴┴┴ ┴ ┴ └──┘ └──┘└────────────┘┴ └──────────┘┴ ┴└─────────┘└──┘└┘
doc └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
txt └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
par └────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘
st └──────────────────────────────────────────────────────────────────────────────────┘└─
37 have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ennreal) = μ s :=
id └─────┘ ┴ ┴
src └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘┴┴ ┴ └───
typ └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘┴┴┴┴ └───
doc └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘ ┴ ┴ └───
txt └─────────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
par └─────────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
pid └──────────────┘└─┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────
38 (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _),
id └───────────────────┘ └──────────┘ └┘
src ───┘ └──┘└───────────────────┘┴ ┴└──────────┘┴ ┴ └─┘
typ ───┘ └──┘└───────────────────┘┴ ┴└──────────┘┴ ┴└┘└─┘
doc ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
txt ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
par ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
pid ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────────┘└─
39 have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ennreal) = ν s :=
id └─────┘ ┴
src └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘ ┴ ┴ └───
typ └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘ ┴┴┴ └───
doc └─────────────────┘ ┴ ┴ ┴ └────────────┘└─────┘└┘ ┴ ┴ └───
txt └─────────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
par └─────────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
pid └──────────────┘└─┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────
40 (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hν _),
id └───────────────────┘ └──────────┘ └┘
src ───┘ └──┘└───────────────────┘┴ ┴└──────────┘┴ ┴ └─┘
typ ───┘ └──┘└───────────────────┘┴ ┴└──────────┘┴ ┴└┘└─┘
doc ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
txt ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
par ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
pid ───┘ └──┘ ┴ ┴ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────────┘└─
41
st ─
42 have d_empty : d ∅ = 0, { simp [d], rw [measure_empty, measure_empty], simp },
id ┴ ┴ ┴ └───────────┘ └───────────┘
src └─────────────┘ ┴┴┴ └┘ └────┘ ┴ └──┘└───────────┘└┘└───────────┘┴ └───┘
typ └─────────────┘┴┴┴┴ └┘ └────┘┴┴ └──┘└───────────┘└┘└───────────┘┴ └───┘
doc └─────────────┘ ┴ ┴ └┘ └────┘ ┴ └──┘ └┘ ┴ └───┘
txt └─────────────┘ ┴ ┴ └┘ └────┘ ┴ └──┘ └┘ ┴ └───┘
par └─────────────┘ ┴ ┴ └┘ └────┘ ┴ └──┘ └┘ ┴ └───┘
pid └──────────┘└─┘ ┴ ┴ ┴┴ ┴┴ ┴ └┘ └┘ ┴ ┴
st ───────────────────────┘└──┘└──────┘└─────────────────┘└─────────────┘└──────┘└┘└
43
st ─
44 have d_split : ∀s t, is_measurable s → is_measurable t →
id └───────────┘ └───────────┘
src └─────────────┘ └─┘ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └
typ └─────────────┘ └─┘ ┴└───────────┘┴ ┴ ┴└───────────┘┴ ┴ └
doc └─────────────┘ └─┘ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └
txt └─────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └
par └─────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └──────────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────────
45 d s = d (s \ t) + d (s ∩ t),
id ┴ ┴ ┴ ┴
src ───┘ ┴ ┴ ┴ ┴ ┴┴┴ └┘┴┴ ┴ ┴┴┴ ┴
typ ───┘ ┴ ┴ ┴ ┴ ┴┴┴ └┘┴┴┴┴ ┴┴┴ ┴
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────┘└─
46 { assume s t hs ht,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └──────────────┘
st ───┘└──────────────┘└─
47 simp only [d],
id ┴
src └─────────┘ ┴
typ └─────────┘┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────┘└─
48 rw [measure_eq_inter_diff hs ht, measure_eq_inter_diff hs ht,
id └───────────────────┘ └┘ └┘ └───────────────────┘ └┘ └┘
src └──┘└───────────────────┘┴ ┴ └┘└───────────────────┘┴ ┴ └─
typ └──┘└───────────────────┘┴└┘┴└┘└┘└───────────────────┘┴└┘┴└┘└─
doc └──┘ ┴ ┴ └┘ ┴ ┴ └─
txt └──┘ ┴ ┴ └┘ ┴ ┴ └─
par └──┘ ┴ ┴ └┘ ┴ ┴ └─
pid └┘ ┴ ┴ └┘ ┴ ┴ └─
st ──────────────────────────────────┘└───────────────────────────┘└─
49 ennreal.to_nnreal_add (hμ _) (hμ _), ennreal.to_nnreal_add (hν _) (hν _),
id └───────────────────┘ └┘ └───────────────────┘ └┘
src ─────┘└───────────────────┘┴ └──┘ └───┘└───────────────────┘┴ └──┘ └────
typ ─────┘└───────────────────┘┴ └──┘ └┘└───┘└───────────────────┘┴ └──┘ └┘└────
doc ─────┘ ┴ └──┘ └───┘ ┴ └──┘ └────
txt ─────┘ ┴ └──┘ └───┘ ┴ └──┘ └────
par ─────┘ ┴ └──┘ └───┘ ┴ └──┘ └────
pid ─────┘ ┴ └──┘ └───┘ ┴ └──┘ └────
st ────────────────────────────────────────┘└───────────────────────────────────┘└─
50 nnreal.coe_add, nnreal.coe_add],
id └────────────┘ └────────────┘
src ─────┘└────────────┘└┘└────────────┘┴
typ ─────┘└────────────┘└┘└────────────┘┴
doc ─────┘ └┘ ┴
txt ─────┘ └┘ ┴
par ─────┘ └┘ ┴
pid ─────┘ └┘ ┴
st ───────────────────┘└──────────────┘└──
51 simp only [sub_eq_add_neg, neg_add],
id └────────────┘ └─────┘
src └─────────┘└────────────┘└┘└─────┘┴
typ └─────────┘└────────────┘└┘└─────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ──────────────────────────────────────┘└─
52 ac_refl },
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───────────┘└┘└
53
st ─
54 have d_Union : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → monotone s →
id ┴ └─┘ ┴ └───────────┘ └──────┘
src └─────────────┘ └───┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴└──────┘┴ ┴ └
typ └─────────────┘ └───┘ ┴┴┴└─┘┴┴┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴└──────┘┴ ┴ └
doc └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴└──────┘┴ ┴ └
txt └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └
par └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └
pid └──────────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └
st ────────────────────────────────────────────────────────────────────────────
55 tendsto (λn, d (s n)) at_top (𝓝 (d (⋃n, s n))),
id └─────┘ └────┘ ┴ ┴ ┴ ┴
src ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴┴ ┴ ┴┴┴┴ ┴ └─┘
typ ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴┴ ┴┴ ┴┴┴┴ ┴ └─┘
doc ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴┴ ┴ ┴┴┴┴ ┴ └─┘
txt ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────┘└─
56 { assume s hs hm,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───┘└────────────┘└─
57 refine tendsto.sub _ _;
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ────────────────────────────
58 refine (nnreal.tendsto_coe.2 $
id └────────────────┘
src └─────┘ └────────────────┘└─┘ └
typ └─────┘ └────────────────┘└─┘ └
doc └─────┘ └─┘ └
txt └─────┘ └─┘ └
par └─────┘ └─┘ └
pid ┴ └─┘ └
st ─────────────────────────────────────
59 (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Union hs hm),
id └───────────────────────┘ └──────────┘ └───────────────────┘ └┘ └┘
src ───────┘ └───────────────────────┘┴ ┴ └──────────┘└─────┘ └───────┘ ┴└───────────────────┘┴ ┴ ┴
typ ───────┘ └───────────────────────┘┴ ┴ └──────────┘└─────┘ └───────┘ ┴└───────────────────┘┴└┘┴└┘┴
doc ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ ┴
txt ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ ┴
par ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ ┴
pid ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
60 exact hμ _,
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────┘└─
61 exact hν _ },
id └┘
src └────┘ └─┘
typ └────┘└┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ──────────────┘└┘└
62
st ─
63 have d_Inter : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → (∀n m, n ≤ m → s m ⊆ s n) →
id └─┘ ┴ └───────────┘ ┴ ┴
src └─────────────┘ └───┘ ┴ ┴└─┘┴ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ └┘ └
typ └─────────────┘ └───┘ ┴ ┴└─┘┴┴┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ └┘ └
doc └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
txt └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
par └─────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
pid └──────────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └
st ───────────────────────────────────────────────────────────────────────────────────────────
64 tendsto (λn, d (s n)) at_top (𝓝 (d (⋂n, s n))),
id └─────┘ └────┘ ┴ ┴ ┴
src ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴┴┴┴ ┴ └─┘
typ ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴ ┴┴ ┴┴┴┴ ┴ └─┘
doc ───┘└─────┘┴ └─┘ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴┴┴┴ ┴ └─┘
txt ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid ───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────┘└─
65 { assume s hs hm,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───┘└────────────┘└─
66 refine tendsto.sub _ _;
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ────────────────────────────
67 refine (nnreal.tendsto_coe.2 $
id └────────────────┘
src └─────┘ └────────────────┘└─┘ └
typ └─────┘ └────────────────┘└─┘ └
doc └─────┘ └─┘ └
txt └─────┘ └─┘ └
par └─────┘ └─┘ └
pid ┴ └─┘ └
st ─────────────────────────────────────
68 (ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _).comp $ tendsto_measure_Inter hs hm _),
id └───────────────────────┘ └──────────┘ └───────────────────┘ └┘ └┘
src ───────┘ └───────────────────────┘┴ ┴ └──────────┘└─────┘ └───────┘ ┴└───────────────────┘┴ ┴ └─┘
typ ───────┘ └───────────────────────┘┴ ┴ └──────────┘└─────┘ └───────┘ ┴└───────────────────┘┴└┘┴└┘└─┘
doc ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ └─┘
txt ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ └─┘
par ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ └─┘
pid ───────┘ ┴ ┴ └─────┘ └───────┘ ┴ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─
69 exact hμ _,
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────┘└─
70 exact ⟨0, hμ _⟩,
id └┘
src └────┘ └─┘ └─┘
typ └────┘ └─┘└┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ──────────────────┘└─
71 exact hν _,
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────┘└─
72 exact ⟨0, hν _⟩ },
id └┘
src └────┘ └─┘ └──┘
typ └────┘ └─┘└┘└──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
pid ┴ └─┘ └─┘┴
st ───────────────────┘└┘└
73
st ─
74 have bdd_c : bdd_above c,
id └───────┘ ┴
src └───────────┘└───────┘┴
typ └───────────┘└───────┘┴┴
doc └───────────┘└───────┘┴
txt └───────────┘ ┴
par └───────────┘ ┴
pid └────────┘└─┘ ┴
st ─────────────────────────┘└─
75 { use (μ univ).to_nnreal,
id ┴ └──┘
src └──┘ ┴└──┘└─────────┘
typ └──┘ ┴┴└──┘└─────────┘
doc └──┘ ┴ └─────────┘
txt └──┘ ┴ └─────────┘
par └──┘ ┴ └─────────┘
pid ┴ ┴ └────────┘┴
st ───┘└────────────────────┘└─
76 rintros r ⟨s, hs, rfl⟩,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └─────────────┘
st ─────────────────────────┘└─
77 refine le_trans (sub_le_self _ $ nnreal.coe_nonneg _) _,
id └──────┘ └─────────┘ └───────────────┘
src └─────┘└──────┘┴ └─────────┘└─┘ ┴└───────────────┘└───┘
typ └─────┘└──────┘┴ └─────────┘└─┘ ┴└───────────────┘└───┘
doc └─────┘ ┴ └─┘ ┴ └───┘
txt └─────┘ ┴ └─┘ ┴ └───┘
par └─────┘ ┴ └─┘ ┴ └───┘
pid ┴ ┴ └─┘ ┴ └───┘
st ──────────────────────────────────────────────────────────┘└─
78 rw [nnreal.coe_le, ← ennreal.coe_le_coe, to_nnreal_μ, to_nnreal_μ],
id └───────────┘ └────────────────┘ └─────────┘ └─────────┘
src └──┘└───────────┘└──┘└────────────────┘└┘ └┘ ┴
typ └──┘└───────────┘└──┘└────────────────┘└┘└─────────┘└┘└─────────┘┴
doc └──┘ └──┘ └┘ └┘ ┴
txt └──┘ └──┘ └┘ └┘ ┴
par └──┘ └──┘ └┘ └┘ ┴
pid └┘ └──┘ └┘ └┘ ┴
st ────────────────────┘└────────────────────┘└───────────┘└───────────┘└──
79 exact measure_mono (subset_univ _) },
id └──────────┘ └─────────┘
src └────┘└──────────┘┴ └─────────┘└──┘
typ └────┘└──────────┘┴ └─────────┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └─┘┴
st ──────────────────────────────────────┘└┘└
80
st ─
81 have c_nonempty : c.nonempty := nonempty.image _ ⟨_, is_measurable.empty⟩,
id └────────┘ └────────────┘ └─────────────────┘
src └────────────────┘└────────┘└──┘└────────────┘└─┘ └─┘└─────────────────┘┴
typ └────────────────┘└────────┘└──┘└────────────┘└─┘ └─┘└─────────────────┘┴
doc └────────────────┘└────────┘└──┘ └─┘ └─┘ ┴
txt └────────────────┘ └──┘ └─┘ └─┘ ┴
par └────────────────┘ └──┘ └─┘ └─┘ ┴
pid └─────────────┘└─┘ └──┘ └─┘ └─┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
82
st ─
83 have d_le_γ : ∀s, is_measurable s → d s ≤ γ := assume s hs, le_cSup bdd_c ⟨s, hs, rfl⟩,
id └───────────┘ ┴ ┴ └─────┘ └───┘ └─┘
src └────────────┘ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘└─────┘┴ ┴ └┘ └┘└─┘┴
typ └────────────┘ ┴ ┴└───────────┘┴ ┴ ┴┴┴ ┴ ┴┴└──┘ └─────┘└─────┘┴└───┘┴ └┘ └┘└─┘┴
doc └────────────┘ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └┘ └┘ ┴
txt └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └┘ └┘ ┴
par └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └┘ └┘ ┴
pid └─────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
84
st ─
85 have : ∀n:ℕ, ∃s : set α, is_measurable s ∧ γ - (1/2)^n < d s,
id ┴ └─┘ ┴┴ └───────────┘ ┴ ┴ ┴ ┴
src └─────┘ └┘ ┴┴└──┘└─┘┴ ┴┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴┴└┘┴ ┴ ┴ ┴
typ └─────┘ └┘ ┴┴└──┘└─┘┴┴┴┴└───────────┘┴ ┴ ┴┴┴ ┴ ┴┴└┘┴ ┴ ┴┴┴
doc └─────┘ └┘ ┴ └──┘ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
86 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
87 have : γ - (1/2)^n < γ := sub_lt_self γ (pow_pos (half_pos zero_lt_one) n),
id ┴ ┴ └─────────┘ ┴ └─────┘ └──────┘ └─────────┘ ┴
src └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘└─────────┘┴ ┴ └─────┘┴ └──────┘┴└─────────┘└┘ ┴
typ └─────┘ ┴ ┴ ┴ └┘ ┴┴ ┴┴└──┘└─────────┘┴┴┴ └─────┘┴ └──────┘┴└─────────┘└┘┴┴
doc └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└─
88 rcases exists_lt_of_lt_cSup c_nonempty this with ⟨r, ⟨s, hs, rfl⟩, hlt⟩,
id └──────────────────┘ └────────┘ └──┘
src └─────┘└──────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└──────────────────┘┴└────────┘┴└──┘└──────────────────────────┘
doc └─────┘└──────────────────┘┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
89 exact ⟨s, hs, hlt⟩ },
id ┴ └┘ └─┘
src └────┘ └┘ └┘ └┘
typ └────┘ ┴└┘└┘└┘└─┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ──────────────────────┘└┘└
90 rcases classical.axiom_of_choice this with ⟨e, he⟩,
id └───────────────────────┘ └──┘
src └─────┘└───────────────────────┘┴ └───────────┘
typ └─────┘└───────────────────────┘┴└──┘└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ───────────────────────────────────────────────────┘└─
91 change ℕ → set α at e,
id └─┘ ┴
src └─────┘ ┴ ┴└─┘┴ └───┘
typ └─────┘ ┴ ┴└─┘┴┴└───┘
doc └─────┘ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ ┴└──┘
st ──────────────────────┘└─
92 have he₁ : ∀n, is_measurable (e n) := assume n, (he n).1,
id └───────────┘ ┴ └┘
src └─────────┘ ┴ ┴└───────────┘┴ ┴ └───┘ └──┘ ┴ └─┘
typ └─────────┘ ┴ ┴└───────────┘┴ ┴┴ └───┘ └──┘ └┘┴ └─┘
doc └─────────┘ ┴ ┴└───────────┘┴ ┴ └───┘ └──┘ ┴ └─┘
txt └─────────┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
par └─────────┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴└──┘ └──┘ ┴ ┴└┘
st ─────────────────────────────────────────────────────────┘└─
93 have he₂ : ∀n, γ - (1/2)^n < d (e n) := assume n, (he n).2,
id ┴ ┴ ┴ └┘
src └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
typ └─────────┘ ┴ ┴┴┴ ┴ ┴ └┘ ┴ ┴┴┴ ┴┴ └───┘ └──┘ └┘┴ └─┘
doc └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴ └─┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴└──┘ └──┘ ┴ ┴└┘
st ───────────────────────────────────────────────────────────┘└─
94
st ─
95 let f : ℕ → ℕ → set α := λn m, (finset.Ico n (m + 1)).inf e,
id └─┘ ┴ └────────┘ ┴
src └──────┘ ┴ ┴ ┴ ┴└─┘┴ └──┘ └───┘ └────────┘┴ ┴ ┴ └───────┘
typ └──────┘ ┴ ┴ ┴ ┴└─┘┴┴└──┘ └───┘ └────────┘┴ ┴ ┴ └───────┘┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ └────────┘┴ ┴ ┴ └───────┘
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └───────┘
par └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └───────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └───────┘
st ────────────────────────────────────────────────────────────┘└─
96
st ─
97 have hf : ∀n m, is_measurable (f n m),
id └───────────┘ ┴
src └────────┘ └─┘ ┴└───────────┘┴ ┴ ┴ ┴
typ └────────┘ └─┘ ┴└───────────┘┴ ┴┴ ┴ ┴
doc └────────┘ └─┘ ┴└───────────┘┴ ┴ ┴ ┴
txt └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
98 { assume n m,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───┘└────────┘└─
99 simp only [f, finset.inf_eq_infi],
id ┴ └────────────────┘
src └─────────┘ └┘└────────────────┘┴
typ └─────────┘┴└┘└────────────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ────────────────────────────────────┘└─
100 exact is_measurable.bInter (countable_encodable _) (assume i _, he₁ _) },
id └──────────────────┘ └─────────────────┘ └─┘
src └────┘└──────────────────┘┴ └─────────────────┘└──┘ └────┘ └──┘
typ └────┘└──────────────────┘┴ └─────────────────┘└──┘ └────┘└─┘└──┘
doc └────┘ ┴ └──┘ └────┘ └──┘
txt └────┘ ┴ └──┘ └────┘ └──┘
par └────┘ ┴ └──┘ └────┘ └──┘
pid ┴ ┴ └──┘ └────┘ └─┘┴
st ──────────────────────────────────────────────────────────────────────────┘└┘└
101
st ─
102 have f_subset_f : ∀{a b c d}, a ≤ b → c ≤ d → f a d ⊆ f b c,
id ┴ ┴ ┴
src └────────────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────────┘ └───────┘ ┴ ┴┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴
doc └────────────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
103 { assume a b c d hab hcd,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └────────────────────┘
st ───┘└────────────────────┘└─
104 dsimp only [f],
id ┴
src └──────────┘ ┴
typ └──────────┘┴┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid └───┘└┘ ┴
st ─────────────────┘└─
105 rw [finset.inf_eq_infi, finset.inf_eq_infi],
id └────────────────┘ └────────────────┘
src └──┘└────────────────┘└┘└────────────────┘┴
typ └──┘└────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────────┘└──────────────────┘└──
106 refine bInter_subset_bInter_left _,
id └───────────────────────┘
src └─────┘└───────────────────────┘└┘
typ └─────┘└───────────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ─────────────────────────────────────┘└─
107 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
108 rintros j ⟨hbj, hjc⟩,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ───────────────────────┘└─
109 exact ⟨le_trans hab hbj, lt_of_lt_of_le hjc $ add_le_add_right hcd 1⟩ },
id └──────┘ └─┘ └─┘ └────────────┘ └─┘ └──────────────┘ └─┘
src └────┘ └──────┘┴ ┴ └┘└────────────┘┴ ┴ ┴└──────────────┘┴ └──┘
typ └────┘ └──────┘┴└─┘┴└─┘└┘└────────────┘┴└─┘┴ ┴└──────────────┘┴└─┘└──┘
doc └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
110
st ─
111 have f_succ : ∀n m, n ≤ m → f n (m + 1) = f n m ∩ e (m + 1),
id ┴ ┴
src └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴┴ ┴ ┴ ┴┴┴ ┴ └─┘
doc └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
txt └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid └─────────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────┘└─
112 { assume n m hnm,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───┘└────────────┘└─
113 have : n ≤ m + 1 := le_of_lt (nat.succ_le_succ hnm),
id ┴ ┴ └──────┘ └──────────────┘ └─┘
src └─────┘ ┴ ┴ ┴ └────┘└──────┘┴ └──────────────┘┴ ┴
typ └─────┘┴┴ ┴┴┴ └────┘└──────┘┴ └──────────────┘┴└─┘┴
doc └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
114 simp only [f],
id ┴
src └─────────┘ ┴
typ └─────────┘┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────┘└─
115 rw [finset.Ico.succ_top this, finset.inf_insert, set.inter_comm],
id └─────────────────┘ └──┘ └───────────────┘ └────────────┘
src └──┘└─────────────────┘┴ └┘└───────────────┘└┘└────────────┘┴
typ └──┘└─────────────────┘┴└──┘└┘└───────────────┘└┘└────────────┘┴
doc └──┘ ┴ └┘ └┘ ┴
txt └──┘ ┴ └┘ └┘ ┴
par └──┘ ┴ └┘ └┘ ┴
pid └┘ ┴ └┘ └┘ ┴
st ───────────────────────────────┘└─────────────────┘└──────────────┘└──
116 refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└┘└
117
st ─
118 have le_d_f : ∀n m, m ≤ n → γ - 2 * ((1 / 2) ^ m) + (1 / 2) ^ n ≤ d (f m n),
id ┴ ┴ ┴ ┴ ┴
src └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────┘ └─┘ ┴ ┴┴┴ ┴ ┴┴┴ └─┘┴┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴┴┴ ┴┴ ┴ ┴
doc └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ └┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
119 { assume n m h,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───┘└──────────┘└─
120 refine nat.le_induction _ _ n h,
id └──────────────┘ ┴ ┴
src └─────┘└──────────────┘└───┘ ┴
typ └─────┘└──────────────┘└───┘┴┴┴
doc └─────┘└──────────────┘└───┘ ┴
txt └─────┘ └───┘ ┴
par └─────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ──────────────────────────────────┘└─
121 { have := he₂ m,
id └─┘ ┴
src └──────┘ ┴
typ └──────┘└─┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ─────┘└───────────┘└─
122 simp only [f],
id ┴
src └─────────┘ ┴
typ └─────────┘┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────┘└─
123 rw [finset.Ico.succ_singleton, finset.inf_singleton],
id └───────────────────────┘ └──────────────────┘
src └──┘└───────────────────────┘└┘└──────────────────┘┴
typ └──┘└───────────────────────┘└┘└──────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────────────┘└────────────────────┘└──
124 exact aux this },
id └─┘ └──┘
src └────┘└─┘┴ ┴
typ └────┘└─┘┴└──┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────┘└┘└
125 { assume n (hmn : m ≤ n) ih,
id ┴ ┴
src └──────────────┘ ┴ ┴ └──┘
typ └──────────────┘┴┴ ┴┴└──┘
doc └──────────────┘ ┴ ┴ └──┘
txt └──────────────┘ ┴ ┴ └──┘
par └──────────────┘ ┴ ┴ └──┘
pid └──────────────┘ ┴ ┴ └──┘
st ──────────────────────────────┘└─
126 have : γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)),
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─────┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴┴┴ ┴┴┴ ┴┴┴┴ ┴┴ └──┘
doc └─────┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
127 { calc γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n+1)) ≤
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────┘└────────────────────────────────────────────────
128 γ + (γ - 2 * (1 / 2)^m + ((1 / 2) ^ n - (1/2)^(n+1))) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────
129 begin
st ─────────┘└─────
130 refine add_le_add_left (add_le_add_left _ _) γ,
id └─────────────┘ ┴
src └─────┘ ┴ └─────────────┘└────┘
typ └─────┘ ┴ └─────────────┘└────┘┴
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ─────────────────────────────────────────────────────────┘└─
131 simp only [pow_add, pow_one, le_sub_iff_add_le],
id └─────┘ └─────┘ └───────────────┘
src └─────────┘└─────┘└┘└─────┘└┘└───────────────┘┴
typ └─────────┘└─────┘└┘└─────┘└┘└───────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────┘└─
132 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────────────
133 end
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└─┘└
134 ... = (γ - (1 / 2)^(n+1)) + (γ - 2 * (1 / 2)^m + (1 / 2)^n) :
st ────────────────────────────────────────────────────────────────────────
135 by simp only [sub_eq_add_neg]; ac_refl
id └────────────┘
src └─────────┘└────────────┘┴ └───────
typ └─────────┘└────────────┘┴ └───────
doc └─────────┘ ┴ └───────
txt └─────────┘ ┴ └───────
par └─────────┘ ┴ └───────
pid ┴└──┘└┘ ┴ └
st ─────────────┘└────────────────────────────────────
136 ... ≤ d (e (n + 1)) + d (f m n) : add_le_add (le_of_lt $ he₂ _) ih
id ┴ ┴ ┴ └────────┘ └──────┘ └─┘ └┘
src ─────────┘ └────────┘ └──────┘
typ ─────────┘ ┴ ┴ ┴ └────────┘ └──────┘ └─┘ └┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└──────────────────────────────────────────────────────────────────
137 ... ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m (n + 1)) :
st ──────────────────────────────────────────────────────────────────────────
138 by rw [f_succ _ _ hmn, d_split (f m n) (e (n + 1)) (hf _ _) (he₁ _), add_assoc]
id └────┘ └─┘ └─────┘ ┴ ┴ ┴ ┴ └┘ └─┘ └───────┘
src └──┘ └───┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘ └───┘└───────┘└─
typ └──┘└────┘└───┘└─┘└┘└─────┘┴ ┴┴┴┴ └┘ ┴┴ ┴┴ └───┘ └┘└────┘ └─┘└───┘└───────┘└─
doc └──┘ └───┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘ └───┘ └─
txt └──┘ └───┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘ └───┘ └─
par └──┘ └───┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘ └───┘ └─
pid └┘ └───┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └────┘ └───┘ ┴└
st ─────────────┘└─────────────────┘└────────────────────────────────────────────┘└─────────┘┴└
139 ... = d (e (n + 1) ∪ f m n) + d (f m (n + 1)) :
id ┴
src ─────────┘ ┴
typ ─────────┘ ┴
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ─────────┘
st ─────────┘└───────────────────────────────────────────────
140 begin
st ───────────┘└─────
141 rw [d_split (e (n + 1) ∪ f m n) (e (n + 1)),
id └─────┘ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────
typ └──┘└─────┘┴ ┴ ┴ └──┘ ┴┴┴┴┴ └┘ ┴┴ ┴┴ └─────
doc └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────
txt └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────
par └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────
pid └┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────
st ────────────────────────────────────────────────────────┘└─
142 union_diff_left, union_inter_cancel_left],
id └─────────────┘ └─────────────────────┘
src ───────────────┘└─────────────┘└┘└─────────────────────┘┴
typ ───────────────┘└─────────────┘└┘└─────────────────────┘┴
doc ───────────────┘ └┘ ┴
txt ───────────────┘ └┘ ┴
par ───────────────┘ └┘ ┴
pid ───────────────┘ └┘ ┴
st ──────────────────────────────┘└───────────────────────┘└──
143 ac_refl,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ────────────────────┘└─
144 exact (he₁ _).union (hf _ _),
id └─┘ └┘
src └────┘ └────────┘ └───┘
typ └────┘ └─┘└────────┘ └┘└───┘
doc └────┘ └────────┘ └───┘
txt └────┘ └────────┘ └───┘
par └────┘ └────────┘ └───┘
pid ┴ └────────┘ └───┘
st ─────────────────────────────────────────┘└─
145 exact (he₁ _)
id └─┘
src └────┘ └───
typ └────┘ └─┘└───
doc └────┘ └───
txt └────┘ └───
par └────┘ └───
pid ┴ └─┘└
st ────────────────────────────
146 end
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ───────────┘
st ───────────┘└─┘└
147 ... ≤ γ + d (f m (n + 1)) :
st ──────────────────────────────────────
148 add_le_add_right (d_le_γ _ $ (he₁ _).union (hf _ _)) _ },
id └──────────────┘ └────┘ └───┘
src └──────────────┘ └───┘
typ └──────────────┘ └────┘ └───┘
st ─────────────────────────────────────────────────────────────────┘└─┘└
149 exact (add_le_add_iff_left γ).1 this } },
id └─────────────────┘ ┴ └──┘
src └────┘ └─────────────────┘┴ └──┘ ┴
typ └────┘ └─────────────────┘┴┴└──┘└──┘┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ──────────────────────────────────────────┘└──┘└
150
st ─
151 let s := ⋃ m, ⋂n, f m n,
id ┴ ┴ ┴ ┴ ┴
src └───────┘┴└┘┴┴┴┴┴┴ ┴ ┴
typ └───────┘┴└┘┴┴┴┴┴┴┴┴ ┴
doc └───────┘┴└┘┴┴┴┴┴┴ ┴ ┴
txt └───────┘ └┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └┘ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
152 have γ_le_d_s : γ ≤ d s,
id ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴
typ └──────────────┘┴┴ ┴┴┴┴
doc └──────────────┘ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴
pid └───────────┘└─┘ ┴ ┴ ┴
st ────────────────────────┘└─
153 { have hγ : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 γ),
id └─────┘ └────┘ ┴
src └────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴ ┴
typ └────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴┴┴
doc └────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴ ┴
txt └────────┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
par └────────┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
st ───┘└────────────────────────────────────────────────────┘└─
154 { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 (γ - 2 * 0)), { simpa },
id └─────┘ └────┘ ┴
src └─────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ └────┘
typ └─────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴ ┴┴ └─┘ └──┘ └────┘
doc └─────────┘└─────┘┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘└────┘┴ ┴ ┴ └─┘ └──┘ └────┘
txt └─────────┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └────┘
par └─────────┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ └────┘
pid └───────┘└┘ ┴ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └─┘ └──┘ ┴
st ─────┘└───────────────────────────────────────────────────────────────┘└──┘└────┘└┘└
155 exact (tendsto_const_nhds.sub $ tendsto_const_nhds.mul $
id └────────────────────┘ └────────────────────┘
src └────┘ └────────────────────┘┴ ┴└────────────────────┘┴ └
typ └────┘ └────────────────────┘┴ ┴└────────────────────┘┴ └
doc └────┘ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────────────
156 tendsto_pow_at_top_nhds_0_of_lt_1
id └───────────────────────────────┘
src ───────┘└───────────────────────────────┘└
typ ───────┘└───────────────────────────────┘└
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ──────────────────────────────────────────
157 (le_of_lt $ half_pos $ zero_lt_one) (half_lt_self zero_lt_one)) },
id └──────┘ └──────┘ └──────────┘ └─────────┘
src ─────────┘ └──────┘┴ ┴└──────┘┴ ┴ └┘ └──────────┘┴└─────────┘└─┘
typ ─────────┘ └──────┘┴ ┴└──────┘┴ ┴ └┘ └──────────┘┴└─────────┘└─┘
doc ─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
txt ─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par ─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
158 have hd : tendsto (λm, d (⋂n, f m n)) at_top (𝓝 (d (⋃ m, ⋂ n, f m n))),
id └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘└─────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴└┘┴┴┴└┘┴┴ ┴ ┴ └─┘
typ └────────┘└─────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴┴ ┴└┘┴┴┴└┘┴┴┴┴ ┴ └─┘
doc └────────┘└─────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴└┘┴┴┴└┘┴┴ ┴ ┴ └─┘
txt └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─┘
par └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─┘
pid └─────┘└─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────────┘└─
159 { refine d_Union _ _ _,
id └─────┘
src └─────┘ └────┘
typ └─────┘└─────┘└────┘
doc └─────┘ └────┘
txt └─────┘ └────┘
par └─────┘ └────┘
pid ┴ └────┘
st ─────┘└──────────────────┘└─
160 { assume n, exact is_measurable.Inter (assume m, hf _ _) },
id └─────────────────┘ └┘
src └──────┘ └────┘└─────────────────┘┴ └──┘ └────┘
typ └──────┘ └────┘└─────────────────┘┴ └──┘└┘└────┘
doc └──────┘ └────┘ ┴ └──┘ └────┘
txt └──────┘ └────┘ ┴ └──┘ └────┘
par └──────┘ └────┘ ┴ └──┘ └────┘
pid └──────┘ ┴ ┴ └──┘ └───┘┴
st ───────┘└──────┘└─────────────────────────────────────────────┘└┘└
161 { exact assume n m hnm, subset_Inter
id └──────────┘
src └────┘ └────────┘└──────────┘└
typ └────┘ └────────┘└──────────┘└
doc └────┘ └────────┘ └
txt └────┘ └────────┘ └
par └────┘ └────────┘ └
pid ┴ └────────┘ └
st ───────────────────────────────────────────
162 (assume i, subset.trans (Inter_subset (f n) i) $ f_subset_f hnm $ le_refl _) } },
id └──────────┘ └──────────┘ ┴ └────────┘ └─────┘
src ─────────┘ └──┘└──────────┘┴ └──────────┘┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴└─────┘└──┘
typ ─────────┘ └──┘└──────────┘┴ └──────────┘┴ ┴┴ └┘ └┘ ┴└────────┘┴ ┴ ┴└─────┘└──┘
doc ─────────┘ └──┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └──┘
txt ─────────┘ └──┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └──┘
par ─────────┘ └──┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └──┘
pid ─────────┘ └──┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└──┘└
163 refine le_of_tendsto_of_tendsto (@at_top_ne_bot ℕ _ _) hγ hd (univ_mem_sets' $ assume m, _),
id └──────────────────────┘ └───────────┘ └┘ └┘ └────────────┘
src └─────┘└──────────────────────┘┴ └───────────┘┴ └────┘ ┴ ┴ └────────────┘┴ ┴ └────┘
typ └─────┘└──────────────────────┘┴ └───────────┘┴ └────┘└┘┴└┘┴ └────────────┘┴ ┴ └────┘
doc └─────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
par └─────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
164 change γ - 2 * (1 / 2) ^ m ≤ d (⋂ (n : ℕ), f m n),
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴┴┴ ┴ ┴ ┴
typ └─────┘┴┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴┴┴ ┴└────┘ ┴┴┴┴┴┴┴ ┴
doc └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴┴┴ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘└─
165 have : tendsto (λn, d (f m n)) at_top (𝓝 (d (⋂ n, f m n))),
id └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────┘┴ └─┘ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴└┘┴┴ ┴ ┴ └─┘
typ └─────┘└─────┘┴ └─┘ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴┴ ┴└┘┴┴┴┴┴┴ └─┘
doc └─────┘└─────┘┴ └─┘ ┴ ┴ ┴ └─┘└────┘┴ ┴ ┴ ┴└┘┴┴ ┴ ┴ └─┘
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────┘└─
166 { refine d_Inter _ _ _,
id └─────┘
src └─────┘ └────┘
typ └─────┘└─────┘└────┘
doc └─────┘ └────┘
txt └─────┘ └────┘
par └─────┘ └────┘
pid ┴ └────┘
st ─────┘└──────────────────┘└─
167 { assume n, exact hf _ _ },
id └┘
src └──────┘ └────┘ └───┘
typ └──────┘ └────┘└┘└───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid └──────┘ ┴ └──┘┴
st ───────┘└──────┘└─────────────┘└┘└
168 { assume n m hnm, exact f_subset_f (le_refl _) hnm } },
id └────────┘ └─────┘ └─┘
src └────────────┘ └────┘ ┴ └─────┘└──┘ ┴
typ └────────────┘ └────┘└────────┘┴ └─────┘└──┘└─┘┴
doc └────────────┘ └────┘ ┴ └──┘ ┴
txt └────────────┘ └────┘ ┴ └──┘ ┴
par └────────────┘ └────┘ ┴ └──┘ ┴
pid └────────────┘ ┴ ┴ └──┘ ┴
st ─────────────────────┘└─────────────────────────────────┘└──┘└
169 refine ge_of_tendsto (@at_top_ne_bot ℕ _ _) this (mem_at_top_sets.2 ⟨m, assume n hmn, _⟩),
id └───────────┘ └───────────┘ └──┘ └─────────────┘ ┴
src └─────┘└───────────┘┴ └───────────┘┴ └────┘ ┴ └─────────────┘└─┘ └┘ └─────────┘
typ └─────┘└───────────┘┴ └───────────┘┴ └────┘└──┘┴ └─────────────┘└─┘ ┴└┘ └─────────┘
doc └─────┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └─────────┘
txt └─────┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └─────────┘
par └─────┘ ┴ ┴ └────┘ ┴ └─┘ └┘ └─────────┘
pid ┴ ┴ ┴ └────┘ ┴ └─┘ └┘ └─────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
170 change γ - 2 * (1 / 2) ^ m ≤ d (f m n),
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘┴┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴┴┴ ┴┴┴┴┴┴
doc └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └─┘ ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
171 refine le_trans _ (le_d_f _ _ hmn),
id └──────┘ └────┘ └─┘
src └─────┘└──────┘└─┘ └───┘ ┴
typ └─────┘└──────┘└─┘ └────┘└───┘└─┘┴
doc └─────┘ └─┘ └───┘ ┴
txt └─────┘ └─┘ └───┘ ┴
par └─────┘ └─┘ └───┘ ┴
pid ┴ └─┘ └───┘ ┴
st ─────────────────────────────────────┘└─
172 exact le_add_of_le_of_nonneg (le_refl _) (pow_nonneg (le_of_lt $ half_pos $ zero_lt_one) _) },
id └────────────────────┘ └─────┘ └────────┘ └──────┘ └──────┘ └─────────┘
src └────┘└────────────────────┘┴ └─────┘└──┘ └────────┘┴ └──────┘┴ ┴└──────┘┴ ┴└─────────┘└───┘
typ └────┘└────────────────────┘┴ └─────┘└──┘ └────────┘┴ └──────┘┴ ┴└──────┘┴ ┴└─────────┘└───┘
doc └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └───┘
txt └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └───┘
par └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └───┘
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
173
st ─
174 have hs : is_measurable s :=
id └───────────┘ ┴
src └────────┘└───────────┘┴ └───
typ └────────┘└───────────┘┴┴└───
doc └────────┘└───────────┘┴ └───
txt └────────┘ ┴ └───
par └────────┘ ┴ └───
pid └─────┘└─┘ ┴ └───
st ───────────────────────────────
175 is_measurable.Union (assume n, is_measurable.Inter (assume m, hf _ _)),
id └─────────────────┘ └─────────────────┘ └┘
src ───┘└─────────────────┘┴ └──┘└─────────────────┘┴ └──┘ └────┘
typ ───┘└─────────────────┘┴ └──┘└─────────────────┘┴ └──┘└┘└────┘
doc ───┘ ┴ └──┘ ┴ └──┘ └────┘
txt ───┘ ┴ └──┘ ┴ └──┘ └────┘
par ───┘ ┴ └──┘ ┴ └──┘ └────┘
pid ───┘ ┴ └──┘ ┴ └──┘ └────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
176 refine ⟨s, hs, _, _⟩,
id ┴ └┘
src └─────┘ └┘ └─────┘
typ └─────┘ ┴└┘└┘└─────┘
doc └─────┘ └┘ └─────┘
txt └─────┘ └┘ └─────┘
par └─────┘ └┘ └─────┘
pid ┴ └┘ └─────┘
st ─────────────────────┘└─
177 { assume t ht hts,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ───┘└─────────────┘└─
178 have : 0 ≤ d t := ((add_le_add_iff_left γ).1 $
id ┴ ┴ └─────────────────┘
src └───────┘ ┴ ┴ └──┘ └─────────────────┘┴ └──┘ └
typ └───────┘ ┴┴┴┴└──┘ └─────────────────┘┴ └──┘ └
doc └───────┘ ┴ ┴ └──┘ ┴ └──┘ └
txt └───────┘ ┴ ┴ └──┘ ┴ └──┘ └
par └───────┘ ┴ ┴ └──┘ ┴ └──┘ └
pid └───┘└──┘ ┴ ┴ └──┘ ┴ └──┘ └
st ───────────────────────────────────────────────────
179 calc γ + 0 ≤ d s : by rw [add_zero]; exact γ_le_d_s
id ┴ ┴ └──────┘ └──────┘
src ─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴└──┘└──────┘┴└┘└────┘ └
typ ─────┘ ┴ ┴ └─┘ ┴┴┴┴└─┘ ┴└──┘└──────┘┴└┘└────┘└──────┘└
doc ─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴└──┘ ┴└┘└────┘ └
txt ─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴└──┘ ┴└┘└────┘ └
par ─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴└──┘ ┴└┘└────┘ └
pid ─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘ └───────┘ └
st ──────────────────────────┘└───────────┘┴└────────────────
180 ... = d (s \ t) + d t : by rw [d_split _ _ hs ht, inter_eq_self_of_subset_right hts]
id └─────┘ └┘ └┘ └───────────────────────────┘ └─┘
src ───────┘└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└──┘ └───┘ ┴ └┘└───────────────────────────┘┴ └─
typ ───────┘└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└──┘└─────┘└───┘└┘┴└┘└┘└───────────────────────────┘┴└─┘└─
doc ───────┘└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└──┘ └───┘ ┴ └┘ ┴ └─
txt ───────┘└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└──┘ └───┘ ┴ └┘ ┴ └─
par ───────┘└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴└──┘ └───┘ ┴ └┘ ┴ └─
pid ───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ └───┘ └───┘ ┴ └┘ ┴ └─
st ───────┘└────────────────────────┘└────────────────────┘└─────────────────────────────────┘┴└
181 ... ≤ γ + d t : add_le_add (d_le_γ _ (hs.diff ht)) (le_refl _)),
id ┴ ┴ └────────┘ └────┘ └─────┘ └┘ └─────┘
src ───────┘└──┘ ┴ ┴ ┴ ┴ └─┘└────────┘┴ └─┘ └─────┘┴ └─┘ └─────┘└──┘
typ ───────┘└──┘ ┴┴┴ ┴ ┴┴└─┘└────────┘┴ └────┘└─┘ └─────┘┴└┘└─┘ └─────┘└──┘
doc ───────┘└──┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └──┘
txt ───────┘└──┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └──┘
par ───────┘└──┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └──┘
pid ───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └──┘
st ───────┘└─────────────────────────────────────────────────────────────┘└─
182 rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, ← nnreal.coe_le],
id └─────────┘ └─────────┘ └────────────────┘ └───────────┘
src └────┘ └──┘ └┘└────────────────┘└──┘└───────────┘┴
typ └────┘└─────────┘└──┘└─────────┘└┘└────────────────┘└──┘└───────────┘┴
doc └────┘ └──┘ └┘ └──┘ ┴
txt └────┘ └──┘ └┘ └──┘ ┴
par └────┘ └──┘ └┘ └──┘ ┴
pid └──┘ └──┘ └┘ └──┘ ┴
st ────────────────────┘└─────────────┘└──────────────────┘└───────────────┘└──
183 simpa only [d, le_sub_iff_add_le, zero_add] using this },
id ┴ └───────────────┘ └──────┘ └──┘
src └──────────┘ └┘└───────────────┘└┘└──────┘└──────┘ ┴
typ └──────────┘┴└┘└───────────────┘└┘└──────┘└──────┘└──┘┴
doc └──────────┘ └┘ └┘ └──────┘ ┴
txt └──────────┘ └┘ └┘ └──────┘ ┴
par └──────────┘ └┘ └┘ └──────┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────┘┴
184 { assume t ht hts,
185 have : d t ≤ 0,
id ┴ ┴
typ ┴ ┴
186 exact ((add_le_add_iff_left γ).1 $
187 calc γ + d t ≤ d s + d t : add_le_add γ_le_d_s (le_refl _)
id ┴ └┘ └┘
typ ┴ └┘ └┘
188 ... = d (s ∪ t) :
189 begin
190 rw [d_split _ _ (hs.union ht) ht, union_diff_right, union_inter_cancel_right,
191 diff_eq_self.2],
192 exact assume a ⟨hat, has⟩, hts hat has
id ┴
typ ┴
193 end
st └─┘
194 ... ≤ γ + 0 : by rw [add_zero]; exact d_le_γ _ (hs.union ht)),
id ┴ └┘
typ ┴ └┘
195 rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, ← nnreal.coe_le],
196 simpa only [d, sub_le_iff_le_add, zero_add] using this }
id ┴
typ ┴
st └─
197 end
st ──┘
198
199 end measure_theory